E:Type, x1, x2:E. tree_leaf(x1) = tree_leaf(x2)  Tree(E)  x1 = x2 

latex

Definitions	P  Q, Prop, Tree(E), tree_leaf(x), x:A. B(x), t  T, if b t else f fi, is_leaf(t), leaf_value(t), Unit, P  Q, P & Q, , b, A, b
Lemmas	assert wf, not wf, bnot wf, leaf value wf, bool wf, is leaf wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, tree leaf wf2, tree wf